perm filename TAKASU.LE3[LET,JMC] blob sn#216855 filedate 1976-05-25 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂AIL Professor S. Takasu↓Research Institute for Mathematical Sciences
↓Kyoto University↓Kyoto, Japan∞

Dear Professor Takasu:

	I was delighted to receive your letter, and the signed
agreement has been forwarded.  As you will see, I couldn't resist exercising
the bureaucratic stamp I got in Kyoto.  When are you visiting
Stanford, with whom, and for how long?

	Enclosed is a preliminary writeup of a new idea of mine
for getting rid of both opaque contexts and quotation marks in
treating knowledge and the modalities.  I have showed it to several
people here and at M.I.T., almost everyone finds the approach
promising.

	Our new KL-10 processor should be working in less than a
month, and we expect a factor of five in speed from it, so there
will be plenty of computing resources for the proof checker, etc.
Bill Glassmire has completed a proof of correctness of the
McCarthy-Painter compiler in FOL, and there are numerous ideas
for improving its applicability to MTC.  Also a graduate student,
Christopher Goad, has a proof that the first two wise men don't
know the colors of their spots.

	We are all looking forward to your visit.
.sgn